Nuprl Lemma : ma-x-equiv_wf
0,22
postcript
pdf
M
:MsgA,
x
:Id,
s1
,
s2
:
M
.state. (
s1
s2
mod
x
)
Prop
latex
Definitions
MsgA
,
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
M
.ds(
x
)
,
x
:
A
B
(
x
)
,
f
(
a
)
,
s
=
t
,
Prop
,
A
,
P
Q
,
State(
ds
)
,
(
s1
s2
mod
x
)
,
M
.state
Lemmas
not
wf
,
ma-ds
wf
,
Id
wf
,
msga
wf
origin
M:MsgA, x:Id, s1, s2:M.state. (s1 
s2 mod x) 
Prop M:MsgA, x:Id, s1, s2:M.state. (s1 s2 mod x) Prop Tx:A. B(x)
B(x)
A
Q s2 mod x)